COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(proof arithx)
C00015 ENDMK
C⊗;
(proof arithx)
(decl (g g1 g2) |ground| variable)
(decl (m m1 m2 n n1 n2) |ground| variable natnum)
(decl (succ pred) |ground→ground| constant nil unary 950)
(decl (+) |ground⊗ground*→ground| functional nil infix 960)    
(decl (*) |ground⊗ground*→ground| functional nil infix 980)
(decl (< ≤ ≥ >) |ground⊗ground→truthval| constant universal infix 800)
(decl (POSP ZEROP) |ground→truthval| constant)
(decl (0 1 2 3 4 5 6 7 8 9) |ground| constant natnum)
(decl (PSI) |ground→truthval| variable)




(axiom |succ 0 =1|)
(lname digitdef domain simpinfo)
(axiom |succ 1 =2|)       
(lname digitdef domain simpinfo)
(axiom |succ 2 =3|)
(lname digitdef domain simpinfo)
(axiom |succ 3 =4|)
(lname digitdef domain simpinfo)
(axiom |succ 4 =5|)
(lname digitdef domain simpinfo)
(axiom |succ 5 =6|)
(lname digitdef domain simpinfo)
(axiom |succ 6 =7|)
(lname digitdef domain simpinfo)
(axiom |succ 7 =8|)
(lname digitdef domain simpinfo)
(axiom |succ 8 =9|)
(lname digitdef domain simpinfo)




(axiom |∀g.posp(g)⊃natnum(g)|)
(lname domain simpinfo)
(axiom |zerop=(λg.g=0)|)
(lname domain simpinfo)
(axiom |∀n.posp(n)≡n≠0|)
(lname domain simpinfo)
(axiom |∀n. pred(succ n) = n|)
(lname pred_def domain simpinfo)


;;; now come the basic peano axioms  :


(axiom |∀n.natnum(succ n)|)
(lname successor peano domain simpinfo)

(axiom |∀n.posp(succ n )|)
(lname successor peano domain simpinfo)

(axiom |∀m n.succ n = succ m  ≡  n=m|)
(lname successor_cancelation successor peano cancel simpinfo)

(axiom |∀PSI.PSI(0)∧(∀n.PSI(n)⊃PSI(succ n)) ⊃ ∀n.PSI(n)|)
(lname natnuminduction peano)




;;; theorems and definitions taken as axioms for further proofs :

(axiom |∀m n.m≠n⊃succ m≠succ n|)
(lname successor simpinfo)

(axiom |∀m n. m+n = if n=0 then m else succ m + pred n|)
(lname plus_def successor simpinfo)

(axiom |∀n.succ n≠n|)
(lname plus_def successor simpinfo)
(axiom |∀n.succ n=n+1|)
(lname plus_def successor simpinfo)
(axiom |∀m n.m + succ n  =  succ(m+n)|)
(lname plus_def successor simpinfo)


;;;      Plus (+) has been declared as an associative functional 

(axiom |∀m n. m+n = n+m|)
(lname commutativity_of_plus commutativity  plusinfo )

(axiom |∀m n.m+n=n ≡ m=0|)
(lname addition_unity unity  plusinfo simpinfo )

(axiom |∀m n n1.m≠n ⊃ m+n1≠n+n1|)
(lname plus_cancelation cancel  plusinfo simpinfo)

(axiom |∀m n.∃n1. n=m ∨ n=m+n1 ∨ n+n1=m |)
(lname plusinfo simpinfo )





;;; ordering definitions and theorems :


(axiom |∀m n n1. m=n+n1 ⊃ m≥n|)
(lname GE_def  order simpinfo )

(axiom |∀m n n1. m=n+n1 ⊃ n≤m|)
(lname LE_def order simpinfo )

(axiom |∀m n. m≥n ≡ n≤m |)
(lname GE_LE_equivalence order simpinfo )

(axiom |∀m n. m≥n ∧ m≠n ⊃ m>n|)
(lname GT_def order simpinfo )

(axiom |∀m n. m≤n ∧ m≠n ⊃ m<n|)
(lname LT_def ordersimpinfo )

(axiom |∀m n. m>n ≡ n<m |)
(lname GT_LT_equivalence order simpinfo )

(axiom |∀m n. m=n ∨ m>n ∨ m<n|)
(lname trichotomy order simpinfo )


(axiom |∀m n n1. m>n1 ∧ n1>n ⊃ m>n| )
(lname GT_transitivity order_trans order simpinfo )
(axiom |∀m n n1. m≥n1 ∧ n1>n ⊃ m>n| )
(lname GT_transitivity order_trans order simpinfo )
(axiom |∀m n n1. m>n1 ∧ n1≥n ⊃ m>n|)
(lname GT_transitivity order_trans order simpinfo )

(axiom |∀m n n1. m≥n1 ∧ n1≥n ⊃ m≥n|)
(lname GE_transitivity order_trans order simpinfo )


(axiom |∀m n n1. m<n1 ∧ n1<n ⊃ m<n|)
(lname LT_transitivity order_trans order simpinfo )
(axiom |∀m n n1. m≤n1 ∧ n1<n ⊃ m<n|)
(lname LT_transitivity order_trans order simpinfo )
(axiom |∀m n n1. m<n1 ∧ n1≤n ⊃ m<n|)
(lname LT_transitivity order_trans order simpinfo )

(axiom |∀m n n1. m≤n1 ∧ n1≤n ⊃ m≤n|)
(lname LE_transitivity order_trans order simpinfo )


(axiom |∀m n. m+n≥m |)
(lname plus_GE order simpinfo )


(axiom |∀m n n1. m>n ⊃ m+n1>n+n1|)
(lname GT_plus_invariance order simpinfo )

(axiom |∀m n n1. m≥n ⊃ m+n1≥n+n1|)
(lname GE_plus_invariance order simpinfo )

(axiom |∀m n n1. m=n ⊃ m+n1=n+n1|)
(lname EQ_plus_invariance order simpinfo )

(axiom |∀m n n1. m≤n ⊃ m+n1≤n+n1|)
(lname LE_plus_invariance order simpinfo )

(axiom |∀m n n1. m<n ⊃ m+n1<n+n1|)
(lname LT_plus_invariance order simpinfo )






(axiom |∀m m1 n n1. m>m1 ∧ n>n1 ⊃ m+n>m1+n1 |)
(lname GT_plus_transitivity order_trans order simpinfo )
(axiom |∀m m1 n n1. m≥m1 ∧ n>n1 ⊃ m+n>m1+n1 |)
(lname GT_plus_transitivity order_trans order simpinfo )
(axiom |∀m m1 n n1. m>m1 ∧ n≥n1 ⊃ m+n>m1+n1 |)
(lname GT_plus_transitivity order_trans order simpinfo )

(axiom |∀m m1 n n1. m≥m1 ∧ n≥n1 ⊃ m+n≥m1+n1 |)
(lname GE_plus_transitivity order_trans order simpinfo )


(axiom |∀m m1 n n1. m<m1 ∧ n<n1 ⊃ m+n<m1+n1 |)
(lname LT_plus_transitivity order_trans order simpinfo )
(axiom |∀m m1 n n1. m≤m1 ∧ n<n1 ⊃ m+n<m1+n1 |)
(lname LT_plus_transitivity order_trans order simpinfo )
(axiom |∀m m1 n n1. m<m1 ∧ n≤n1 ⊃ m+n<m1+n1 |)
(lname LT_plus_transitivity order_trans order simpinfo )

(axiom |∀m m1 n n1. m≤m1 ∧ n≤n1 ⊃ m+n≤m1+n1 |)
(lname LE_plus_transitivity order_trans order simpinfo )


(axiom |∀m. m≥0|)
(lname Zero_minimal order simpinfo )


(axiom |∀m n. m>n ⊃ m≥n+1|)
(lname GT_to_GE order simpinfo )

(axiom |∀m n. m<n+1 ⊃ m≤n |)
(lname LT_to_LE order simpinfo )



(axiom |∀PSI.(∃m.PSI(m)) ⊃ (∃n. PSI(n) ∧ (∀n1. PSI(n1) ⊃ n≤n1)) |)
(lname property_minimal )

(axiom |∀PSI.∀n.(∀m.m<n ⊃ PSI(m)) ⊃ ∀n.PSI(n)|)
(lname complete_natnum_induction )



;;; we now introduce multiplication :

(axiom |∀m n. m*n = if n=0 then 0 else m * pred n + m|)
(lname  multinfo mult_def simpinfo )

(axiom |∀n. n*0=0|)
(lname zero_mult_def multinfo mult_def simpinfo )

(axiom |∀m n. m * succ n  =  m*n + m  |)
(lname successor_mult_def multinfo mult_def simpinfo )


(axiom |∀n. n*1=n|)
(lname mult_unity unity multinfo  simpinfo )


;;;      Mult (*) is defined to be an associative functional 


(axiom |∀m n. m*n = n*m |)
(lname commutativity_of_mult commutativity multinfo)



(axiom |∀m n n1. m*(n+n1)=m*n+m*n1 |)
(lname distributivity )
(axiom |∀m n n1. (n+n1)*m=n*m+n1*m |)
(lname distributivity )




(axiom |∀m n n1. m=n ⊃ m*n1=n*n1   |)
(lname EQ_mult_invariance order_mult simpinfo )


(axiom |∀m n n1. m≥n ⊃ m*n1≥n*n1   |)
(lname GE_mult_invariance order_mult simpinfo )

(axiom |∀m n n1. posp(n1) ∧ m>n ⊃ m*n1>n*n1 |)
(lname GT_mult_invariance order_mult simpinfo )

(axiom |∀m n n1. m≤n ⊃ m*n1≤n*n1 |)
(lname LE_mult_invariance order_mult simpinfo )

(axiom |∀m n n1. posp(n1) ∧ m<n ⊃ m*n1<n*n1 |)
(lname LT_mult_invariance order_mult simpinfo )



(axiom |∀m n n1. m*n1>n*n1 ⊃ m>n   |)
(lname GT_mult_cancelation cancel order_mult simpinfo )

(axiom |∀m n n1. posp(n1) ∧ m*n1≥n*n1 ⊃ m≥n   |)
(lname GE_mult_cancelation cancel order_mult simpinfo )

(axiom |∀m n n1. m*n1<n*n1 ⊃ m<n   |)
(lname LT_mult_cancelation cancel order_mult simpinfo )

(axiom |∀m n n1. posp(n1) ∧ m*n1≤n*n1 ⊃ m≤n   |)
(lname LE_mult_cancelation cancel order_mult simpinfo )

(axiom |∀m n n1. posp(n1) ∧ m*n1=n*n1 ⊃ m=n   |)
(lname EQ_mult_cancelation cancel order_mult simpinfo )



(axiom |∀m m1 n n1. m>m1 ∧ n>n1 ⊃ m*n>m1*n1|)
(lname GT_mult_transitivity trans multinfo simpinfo )
(axiom |∀m m1 n n1. m≥m1 ∧ n>n1 ⊃ m*n>m1*n1|)
(lname GT_mult_transitivity trans multinfo simpinfo )
(axiom |∀m m1 n n1. m>m1 ∧ n≥n1 ⊃ m*n>m1*n1|)
(lname GT_mult_transitivity trans multinfo simpinfo )

(axiom |∀m m1 n n1. m≥m1 ∧ n≥n1 ⊃ m*n≥m1*n1|)
(lname GE_mult_transitivity trans multinfo simpinfo )


(axiom |∀m m1 n n1. m<m1 ∧ n<n1 ⊃ m*n<m1*n1|)
(lname LT_mult_transitivity trans multinfo simpinfo )
(axiom |∀m m1 n n1. m≤m1 ∧ n<n1 ⊃ m*n<m1*n1|)
(lname LT_mult_transitivity trans multinfo simpinfo )
(axiom |∀m m1 n n1. m<m1 ∧ n≤n1 ⊃ m*n<m1*n1|)
(lname LT_mult_transitivity trans multinfo simpinfo )

(axiom |∀m m1 n n1. m≤m1 ∧ n≤n1 ⊃ m*n≤m1*n1|)
(lname LE_mult_transitivity trans multinfo simpinfo )